Add various specs for HashSet, FSet, and iterators (ranges, filter_map, rev) #1313
Conversation
…p, rev) - Also strengthen the spec of filter Note: the spec for `Borrow` is required for `HashSet::contains`
|
This contains quite a lot of new specifications that need to be discussed. For example, I am not so sure the spec for double ended iterators is the one we want, because it does not say anything about how the forward and the backward relation interact. |
|
The current spec for double ended iterators is at least enough for reasoning about simple and common My understanding is that we're not too happy with the iterator specs as a whole (we'd like either better handling of existentials or to rework the specs to make proofs easier) so I'm wary of putting too much work into iterator specs up front. My approach is more to develop just what is needed by examples I come across. It's better to have some specs than none especially for iterators since Creusot can't translate |
Note: the spec for
Borrowis required forHashSet::contains